Inference at * 1 
Iof proof for Lemma minus functionality wrt le:



1. i : 
2. j : 
3. i  j 
  (-i)  (-j) 

latex

 by InvertRel 3 

latex

 1: 

 1: 3. j  i
 1:   (-i)  (-j)
 .

Definitions

i  j